unsolvable M.pre(a,s) == P != 1of(2of(2of(2of(M))))(a)  v:M.da(locl(a)). P(s,v) 

latex

---

clarification:

unsolvable M.pre(a,s)
== fpf-val(IdDeq; 1of(2of(2of(2of(M)))); a; a,P.(v:M.da(locl(a)). P(s,v))) 

latex

Definitions	z != f(x)  P(a;z), IdDeq, 1of(t), 2of(t), x:A. B(x), M.da(a), locl(a), A
FDL editor aliases	ma-npre